/-
Copyright (c) 2022 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen, Alex J. Best
-/
import Mathlib.LinearAlgebra.FreeModule.PID
import Mathlib.RingTheory.DedekindDomain.PID
import Mathlib.RingTheory.Localization.NormTrace
import Mathlib.RingTheory.IntegralClosure.IntegralRestrict

/-!

# Ideal norms

This file defines the relative ideal norm `Ideal.spanNorm R (I : Ideal S) : Ideal S` as the ideal
spanned by the norms of elements in `I`.

## Main definitions

* `Ideal.spanNorm R (I : Ideal S)`: the ideal spanned by the norms of elements in `I`.
  This is used to define `Ideal.relNorm`.
* `Ideal.relNorm R (I : Ideal S)`: the relative ideal norm as a bundled monoid-with-zero morphism,
  defined as the ideal spanned by the norms of elements in `I`.

## Main results

* `map_mul Ideal.relNorm`: multiplicativity of the relative ideal norm
-/

open scoped nonZeroDivisors

section SpanNorm

namespace Ideal

open Submodule

attribute [local instance] FractionRing.liftAlgebra

variable (R S : Type*) [CommRing R] [IsDomain R] {S : Type*} [CommRing S] [IsDomain S]
variable [IsIntegrallyClosed R] [IsIntegrallyClosed S] [Algebra R S] [Module.Finite R S]
variable [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)]

/-- `Ideal.spanNorm R (I : Ideal S)` is the ideal generated by mapping `Algebra.intNorm R S`
over `I`.

See also `Ideal.relNorm`.
-/
noncomputable def spanNorm (I : Ideal S) : Ideal R :=
  Ideal.map (Algebra.intNorm R S) I

@[simp]
theorem spanNorm_bot :
    spanNorm R (⊥ : Ideal S) = ⊥ := span_eq_bot.mpr fun x hx => by simpa using hx

variable {R} in
@[simp]
theorem spanNorm_eq_bot_iff {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥ := by
  simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map,
    mem_bot]

theorem intNorm_mem_spanNorm {I : Ideal S} {x : S} (hx : x ∈ I) :
    Algebra.intNorm R S x ∈ I.spanNorm R :=
  subset_span (Set.mem_image_of_mem _ hx)

theorem norm_mem_spanNorm [Module.Free R S] {I : Ideal S} (x : S) (hx : x ∈ I) :
    Algebra.norm R x ∈ I.spanNorm R := by
  refine subset_span ⟨x, hx, ?_⟩
  rw [Algebra.intNorm_eq_norm]

@[simp]
theorem spanNorm_singleton {r : S} :
    spanNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
  le_antisymm
    (span_le.mpr fun x hx =>
      mem_span_singleton.mpr
        (by
          obtain ⟨x, hx', rfl⟩ := (Set.mem_image _ _ _).mp hx
          exact map_dvd _ (mem_span_singleton.mp hx')))
    ((span_singleton_le_iff_mem _).mpr (intNorm_mem_spanNorm _ (mem_span_singleton_self _)))

@[simp]
theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by
  simp [← Ideal.span_singleton_one]

theorem map_spanIntNorm (I : Ideal S) {T : Type*} [Semiring T] (f : R →+* T) :
    map f (spanNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) := by
  rw [spanNorm]
  nth_rw 2 [map]
  simp [map_span, Set.image_image]

@[mono]
theorem spanNorm_mono {I J : Ideal S} (h : I ≤ J) : spanNorm R I ≤ spanNorm R J :=
  Ideal.span_mono (Set.monotone_image h)

theorem spanIntNorm_localization (I : Ideal S) (M : Submonoid R) (hM : M ≤ R⁰)
    {Rₘ : Type*} (Sₘ : Type*) [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ]
    [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
    [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
    [IsIntegrallyClosed Rₘ] [IsDomain Rₘ] [IsDomain Sₘ] [NoZeroSMulDivisors Rₘ Sₘ]
    [Module.Finite Rₘ Sₘ] [IsIntegrallyClosed Sₘ]
    [Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)] :
    spanNorm Rₘ (I.map (algebraMap S Sₘ)) = (spanNorm R I).map (algebraMap R Rₘ) := by
  let K := FractionRing R
  let f : Rₘ →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
  let L := FractionRing S
  let g : Sₘ →+* L := IsLocalization.map _ (M := Algebra.algebraMapSubmonoid S M) (T := S⁰)
      (RingHom.id S) (Submonoid.map_le_of_le_comap _ <| hM.trans
      (nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _
        (FaithfulSMul.algebraMap_injective _ _)))
  algebraize [f, g, (algebraMap K L).comp f]
  have : IsScalarTower R Rₘ K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Rₘ K
  have : IsScalarTower S Sₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
  have : IsScalarTower Rₘ Sₘ L := by
    apply IsScalarTower.of_algebraMap_eq'
    apply IsLocalization.ringHom_ext M
    rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Sₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R S Sₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
  let _ := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization
    (Algebra.algebraMapSubmonoid S M) Sₘ L
  have : IsIntegralClosure Sₘ Rₘ L :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
  rw [map_spanIntNorm]
  refine span_eq_span (Set.image_subset_iff.mpr ?_) (Set.image_subset_iff.mpr ?_)
  · intro a' ha'
    simp only [Set.mem_preimage, submodule_span_eq, ← map_spanIntNorm, SetLike.mem_coe,
      IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S M) Sₘ,
      IsLocalization.mem_map_algebraMap_iff M Rₘ, Prod.exists] at ha' ⊢
    obtain ⟨⟨a, ha⟩, ⟨_, ⟨s, hs, rfl⟩⟩, has⟩ := ha'
    refine ⟨⟨Algebra.intNorm R S a, intNorm_mem_spanNorm _ ha⟩,
      ⟨s ^ Module.finrank K L, pow_mem hs _⟩, ?_⟩
    simp only [Submodule.coe_mk, Subtype.coe_mk, map_pow] at has ⊢
    apply_fun algebraMap _ L at has
    apply_fun Algebra.norm K at has
    simp only [map_mul, IsScalarTower.algebraMap_apply R Rₘ Sₘ] at has
    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L,
      Algebra.norm_algebraMap] at has
    apply IsFractionRing.injective Rₘ K
    simp only [map_mul, map_pow]
    have : FiniteDimensional K L := Module.Finite_of_isLocalization R S _ _ R⁰
    rwa [Algebra.algebraMap_intNorm (L := L), ← IsScalarTower.algebraMap_apply,
      ← IsScalarTower.algebraMap_apply, Algebra.algebraMap_intNorm (L := L)]
  · intro a ha
    rw [Set.mem_preimage, Function.comp_apply, Algebra.intNorm_eq_of_isLocalization
      (A := R) (B := S) M (Aₘ := Rₘ) (Bₘ := Sₘ)]
    exact subset_span (Set.mem_image_of_mem _ (mem_map_of_mem _ ha))

theorem spanNorm_mul_spanNorm_le (I J : Ideal S) :
    spanNorm R I * spanNorm R J ≤ spanNorm R (I * J) := by
  rw [spanNorm, spanNorm, spanNorm]
  nth_rw 1 [map]; nth_rw 1 [map]
  rw [Ideal.span_mul_span', ← Set.image_mul]
  refine Ideal.span_mono (Set.monotone_image ?_)
  rintro _ ⟨x, hxI, y, hyJ, rfl⟩
  exact Ideal.mul_mem_mul hxI hyJ

/-- This condition `eq_bot_or_top` is equivalent to being a field.
However, `Ideal.spanNorm_mul_of_field` is harder to apply since we'd need to upgrade a `CommRing R`
instance to a `Field R` instance. -/
theorem spanNorm_mul_of_bot_or_top (eq_bot_or_top : ∀ I : Ideal R, I = ⊥ ∨ I = ⊤) (I J : Ideal S) :
    spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
  refine le_antisymm ?_ (spanNorm_mul_spanNorm_le R _ _)
  rcases eq_bot_or_top (spanNorm R I) with hI | hI
  · rw [hI, spanNorm_eq_bot_iff.mp hI, bot_mul, spanNorm_bot]
    exact bot_le
  rw [hI, Ideal.top_mul]
  rcases eq_bot_or_top (spanNorm R J) with hJ | hJ
  · rw [hJ, spanNorm_eq_bot_iff.mp hJ, mul_bot, spanNorm_bot]
  rw [hJ]
  exact le_top

variable [IsDedekindDomain R] [IsDedekindDomain S]

/-- Multiplicativity of `Ideal.spanNorm`. simp-normal form is `map_mul (Ideal.relNorm R)`. -/
theorem spanNorm_mul (I J : Ideal S) : spanNorm R (I * J) = spanNorm R I * spanNorm R J := by
  nontriviality R
  cases subsingleton_or_nontrivial S
  · have : ∀ I : Ideal S, I = ⊤ := fun I ↦ Subsingleton.elim I ⊤
    simp [this I, this J, this (I * J)]
  refine eq_of_localization_maximal (fun P hP ↦ ?_)
  by_cases hP0 : P = ⊥
  · subst hP0
    rw [spanNorm_mul_of_bot_or_top]
    intro I
    exact or_iff_not_imp_right.mpr fun hI ↦ (hP.eq_of_le hI bot_le).symm
  let P' := Algebra.algebraMapSubmonoid S P.primeCompl
  let Rₚ := Localization.AtPrime P
  let Sₚ := Localization P'
  let _ : Algebra Rₚ Sₚ := localizationAlgebra P.primeCompl S
  have : IsScalarTower R Rₚ Sₚ :=
    IsScalarTower.of_algebraMap_eq (fun x =>
      (IsLocalization.map_eq (T := P') (Q := Localization P') P.primeCompl.le_comap_map x).symm)
  have h : P' ≤ S⁰ :=
    map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)
      P.primeCompl_le_nonZeroDivisors
  have : IsDomain Sₚ := IsLocalization.isDomain_localization h
  have : IsDedekindDomain Sₚ := IsLocalization.isDedekindDomain S h _
  have : IsPrincipalIdealRing Sₚ :=
    IsDedekindDomain.isPrincipalIdealRing_localization_over_prime S P hP0
  have := NoZeroSMulDivisors_of_isLocalization R S Rₚ Sₚ P.primeCompl_le_nonZeroDivisors
  have := Module.Finite_of_isLocalization R S Rₚ Sₚ P.primeCompl
  let L := FractionRing S
  let g : Sₚ →+* L := IsLocalization.map _ (M := P') (T := S⁰) (RingHom.id S) h
  algebraize [g]
  have : IsScalarTower S Sₚ (FractionRing S) := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHom.comp_id])
  have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization P' Sₚ (FractionRing S)
  have : Algebra.IsSeparable (FractionRing Rₚ) (FractionRing Sₚ) := by
    apply Algebra.IsSeparable.of_equiv_equiv
      (FractionRing.algEquiv Rₚ (FractionRing R)).symm.toRingEquiv
      (FractionRing.algEquiv Sₚ (FractionRing S)).symm.toRingEquiv
    apply IsLocalization.ringHom_ext R⁰
    ext
    simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp,
      RingHom.coe_coe, Function.comp_apply, ← IsScalarTower.algebraMap_apply]
    rw [IsScalarTower.algebraMap_apply R Rₚ (FractionRing R), AlgEquiv.coe_ringEquiv,
      AlgEquiv.commutes, IsScalarTower.algebraMap_apply R S L,
      IsScalarTower.algebraMap_apply S Sₚ L, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes]
    simp only [← IsScalarTower.algebraMap_apply]
  simp only [Ideal.map_mul, ← spanIntNorm_localization (R := R) (S := S)
    (Rₘ := Localization.AtPrime P) (Sₘ := Localization P') _ _ P.primeCompl_le_nonZeroDivisors]
  rw [← (I.map _).span_singleton_generator, ← (J.map _).span_singleton_generator,
    span_singleton_mul_span_singleton, spanNorm_singleton, spanNorm_singleton,
    spanNorm_singleton, span_singleton_mul_span_singleton, map_mul]

/-- The relative norm `Ideal.relNorm R (I : Ideal S)`, where `R` and `S` are Dedekind domains,
and `S` is an extension of `R` that is finite and free as a module. -/
noncomputable def relNorm : Ideal S →*₀ Ideal R where
  toFun := spanNorm R
  map_zero' := spanNorm_bot R
  map_one' := by rw [one_eq_top, spanNorm_top R, one_eq_top]
  map_mul' := spanNorm_mul R

theorem relNorm_apply (I : Ideal S) :
    relNorm R I = span (Algebra.intNorm R S '' (I : Set S) : Set R) :=
  rfl

@[simp]
theorem spanNorm_eq (I : Ideal S) : spanNorm R I = relNorm R I := rfl

@[simp]
theorem relNorm_bot : relNorm R (⊥ : Ideal S) = ⊥ := by
  simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

@[simp]
theorem relNorm_top : relNorm R (⊤ : Ideal S) = ⊤ := by
  simpa only [one_eq_top] using map_one (relNorm R : Ideal S →*₀ _)

variable {R} in
@[simp]
theorem relNorm_eq_bot_iff {I : Ideal S} : relNorm R I = ⊥ ↔ I = ⊥ :=
  spanNorm_eq_bot_iff

theorem norm_mem_relNorm [Module.Free R S] (I : Ideal S) {x : S} (hx : x ∈ I) :
    Algebra.norm R x ∈ relNorm R I :=
  norm_mem_spanNorm R x hx

@[simp]
theorem relNorm_singleton (r : S) : relNorm R (span ({r} : Set S)) = span {Algebra.intNorm R S r} :=
  spanNorm_singleton R

theorem map_relNorm (I : Ideal S) {T : Type*} [Semiring T] (f : R →+* T) :
    map f (relNorm R I) = span (f ∘ Algebra.intNorm R S '' (I : Set S)) :=
  map_spanIntNorm R I f

@[mono]
theorem relNorm_mono {I J : Ideal S} (h : I ≤ J) : relNorm R I ≤ relNorm R J :=
  spanNorm_mono R h

end Ideal

end SpanNorm
